Section: Scientific Foundations

Software infrastructure

The Sardes approach to software infrastructure is both architecture-based and language-based: architecture-based for it relies on an explicit component structure for runtime reconfiguration, and language-based for it relies on a high-level type safe programming language as a basis for operating system and middleware construction. Exploiting high-level programming languages for operating system construction [91] has a long history, with systems such as Oberon [95] , SPIN [43] or JX [57] . More recent and relevant developments for Sardes are:

• The developments around the Singularity project at Microsoft Research [55] , [63] , which illustrates the use of language-based software isolation for building a secure operating system kernel.

• The seL4 project [58] , [68] , which developed a formal verification of a modern operating system microkernel using the Isabelle/HOL theorem prover.

• The development of operating system kernels for multicore hardware architectures such as Corey [46] and Barrelfish [42] .

• The development of efficient run-time for event-based programming on multicore systems such as libasync [96] , [70] .